the_es:event_system{i:l}. trans(es-E(the_es); x,y.es-le(the_es; x; y)) 

latex

Definitions	x:A. B(x), trans(T; x,y.E(x;y)), es-le(es; e; e'), P  Q, P  Q, t  T, prop{i:l}, guard(T)
Lemmas	es-locl-trans, es-locl wf, es-E wf, event system wf